A, B, C:Type, g:(A(B + Top)), f:(ABC). f o' g  A(C + Top) 

latex

ProofTree

Definitions	x:AB(x), t  T, x:A. B(x), S  T, Top, left + right, f(a), P  Q, do-apply(f;x), inl x , , b, A, b, s = t, , x:A  B(x), P & Q, P  Q, Unit, Type, x.A(x), suptype(S; T), can-apply(f;x), if b then t else f fi , Void, x:A.B(x), f o' g, False, inr x , True
Lemmas	true wf, false wf, top wf, ifthenelse wf, can-apply wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, do-apply wf